T:Type, P:(T), L:(T List). l_all(L; T; x.(P(x)))  sqequal(filter(P; L); L) 

latex

Definitions	x. t(x), prop{i:l}, t  T, x(s), P  Q, x:A. B(x), P  Q, P  Q, False, A
Lemmas	not wf, bnot wf, assert wf, l all cons, bool wf